FDL - Nuprl Lemma : div_lbound_1

Nuprl Lemma : div_lbound_1

a:

, n:

, k:

. (k

(a

n))

((k * n)

a)

Up int 2, int 2

Definitions t T, x:A. B(x), P Q, P Q, P & Q, P Q, False, A, A B, x:A. B(x), , , Div(a;n;q), i j < k, , S T

Lemmas nat plus wf, nat wf, div elim, le wf, iff wf, nat plus inc, mul preserves le, lt transitivity 2, mul com, mul cancel in lt